The proof relies on two auxiliary results:
completeness (Lemma \ref{l:compl-pas}) and soundness (Lemma \ref{l:sound-pas}).
We begin by defining the encoding of \mm configuration into \evol{1}. 
\begin{definition}\label{def:confe1}
Let $N$ be a \mm 
with 
registers $r_j ~(j \in \{0,1\})$ and 
instructions $(1:I_1), \ldots, (n:I_n)$.
The encoding of a configuration $(i,m_0, m_1)$ of $N$, denoted
$\encp{(i, m_{0}, m_{1})}{\mmn{1}}$, is defined as:
\[
 \outC{p_i} \parallel \encp{r_0 = m_0}{\mmn{1}} \parallel \encp{r_1 = m_1}{\mmn{1}} \parallel \prod^{n}_{i=1} \encp{(i:I_i)}{\mmn{1}}
\]
where the encodings 
$\encp{r_j = m_j}{\mmn{1}}$ and  
$\encp{(i:I_i)}{\mmn{1}}, \ldots, \encp{(n:I_n)}{\mmn{1}}$ are as in Table~\ref{t:encod-pas}.
\end{definition}


\begin{lemma}[Completeness]\label{l:compl-pas}
Let $(i, m_0, m_1)$ be a configuration of a \mm $N$. 
\begin{enumerate}
\item  If $(i, m_0, m_1)\minskred (i', m_0', m_1')$ then, for some process $P$, 
it holds that\\ $\encp{(i, m_0, m_1) }{\mmn{1}} \pired^* P \equiv \encp{(i', m_0', m_1') }{\mmn{1}}$.

\item If  $(i, m_0, m_1)\notminskred $ then $\encp{(i, m_0, m_1) }{\mmn{1}} \barbk{e}$
\end{enumerate}

\end{lemma}

\begin{proof}
\underline{\emph{Item (1)}:} 
We proceed by a case analysis on the instruction  performed by the \mma.
Hence, we distinguish three cases corresponding to the behaviors associated to rules
\textsc{M-Inc}, \textsc{M-Dec}, and \textsc{M-Jmp}.
Without loss of generality, we restrict our analysis to operations on register $r_0$.

\begin{description}
 \item[Case \textsc{M-Inc}:] We have a Minsky configuration $(i, m_0, m_1)$ with 
$(i: \mathtt{INC}(r_0))$. By Definition \ref{def:confe1}, its encoding into \evol{1} is as follows:
\begin{align*}
\encp{(i, m_0, m_1)}{\mmn{1}}  =   & ~\overline{p_i} \parallel \encp{r_0 = m_0}{\mmn{1}} \parallel \encp{r_1 = m_1}{\mmn{1}} \parallel  \\
&  \encp{(i: \mathtt{INC}(r_0))}{\mmn{1}} \parallel   \prod_{l=1..n,l\not = i} \encp{(l:I_l)}{\mmn{1}} 
\end{align*}

After consuming the program counter $p_i$  we have the following 
\[
\encp{(i, m_0, m_1)}{\mmn{1}}  \pired 
\component{r_0}{\encn{m_{0}}{0}} \parallel \update{r_0}{\component{r_0}{\overline{u_{0}}.\bullet}}.\overline{p_{i+1}}
\parallel S = P_1
\]
where $S = \encp{r_1 = m_1}{\mmn{1}} \parallel \prod_{i=1}^n \encp{(i:I_i)}{\mmn{1}}$ stands for the rest of the system.
The only reduction possible at this point is the synchronization on $r_0$, which allows 
the update of  the adaptable process at  $r_0$:
\[
 P_1 \pired \component{r_0}{\overline{u_{0}}.\encn{m_{0}}{0}} \parallel \overline{p_{i+1}} \parallel S = P_2 \, .
\]
By the encoding of numbers, it 
$P_{2}$ can be equivalently written as
\[
\component{r_0}{\encn{m_{0}+1}{0}} \parallel \overline{p_{i+1}} \parallel S
\]
and so it is easy to see that $P_2 \equiv \encp{(i+1, m_0+1, m_1)}{\mmn{1}}$, as desired. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\item[Case \textsc{M-Dec}:] We have a Minsky configuration $(i, c, m_1)$ such that 
$(i: \mathtt{DEC}(r_0,s))$ and $c > 0$. By Definition \ref{def:confe1}, its encoding into \evol{1}  is as follows:
\begin{eqnarray*}
\encp{(i, c, m_1)}{\mmn{1}} & = &   \overline{p_i} \parallel \encp{r_0 = c}{\mmn{1}} \parallel \encp{r_1 = m_1}{\mmn{1}} \parallel  \\
& & \encp{(i: \mathtt{DEC}(r_0,s))}{\mmn{1}} \parallel   \prod_{l=1..n,l\not = i} \encp{(l:I_l)}{\mmn{1}} 
\end{eqnarray*}
We begin by consuming the program counter $p_i$, which leaves the content of $\encp{(i: \mathtt{DEC}(r_0,s))}{\mmn{1}}$ exposed.
Using the encoding of numbers we have the following:
\[
 \encp{(i, c, m_1)}{\mmn{1}}  \pired   \component{r_0}{\overline{u_0}.\encn{c-1}{0}}
 \parallel (u_0.\overline{p_{i+1}} + z_0.\update{r_0}{\component{r_0}{\overline{z_0}}}.\overline{p_{s}}) \parallel S = P_1
\]
where $S = \encp{r_1 = m_1}{\mmn{1}} \parallel \prod_{i=1}^n \encp{(i:I_i)}{\mmn{1}}$ stands for the rest of the system.
Notice that only reduction possible at this point is the synchronization on $u_0$, 
which signals the fact we are performing a decrement instruction.
After this synchronization we have 
\begin{eqnarray*}
 P_1 & \pired  & \component{r_0}{\encn{c-1}{0}} \parallel \overline{p_{i+1}}  \parallel S \\
 & \equiv &  \encp{(i+1, c-1, m_1)}{\mmn{1}} 
\end{eqnarray*}
as desired.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\item[Case \textsc{M-Jmp}:] We have a Minsky configuration $(i, 0, m_1)$ and 
$(i: \mathtt{DEC}(r_0,s))$. By Definition \ref{def:confe1}, 
its encoding into \evol{1} is as follows:
\begin{eqnarray*}
\encp{(i, 0, m_1)}{\mmn{1}} & = &   \overline{p_i} \parallel \encp{r_0 = 0}{\mmn{1}} \parallel \encp{r_1 = m_1}{\mmn{1}} \parallel  \\
& & \encp{(i: \mathtt{DEC}(r_0,s))}{\mmn{1}} \parallel   \prod_{l=1..n,l\not = i} \encp{(l:I_l)}{\mmn{1}} \, .
\end{eqnarray*}
We begin by consuming the program counter $p_i$, which leaves the content of $\encp{(i: \mathtt{DEC}(r_0,s))}{\mmn{1}}$ exposed.
Using the encoding of numbers we have the following:
\[
 \encp{(i, 0, m_1)}{\mmn{1}}  \pired   \component{r_0}{\overline{z_0}}
 \parallel (u_0.\overline{p_{i+1}} + z_0.\update{r_0}{\component{r_0}{\overline{z_0}}}.\overline{p_{s}}) \parallel S = P_1
\]
where $S = \encp{r_1 = m_1}{\mmn{1}} \parallel \prod_{i=1}^n \encp{(i:I_i)}{\mmn{1}}$ stands for the rest of the system.
In $P_1$, the only reduction possible is through a synchronization on $z_0$, 
which signals the fact we are performing a jump.
Such a synchronization, in turn, enables an update action on $r_0$.
We then have:
\begin{eqnarray*}
P_1 & \pired &  \component{r_0}{\nil} \parallel \update{r_0}{\component{r_0}{\overline{z_0}}}.\overline{p_{s}} \parallel S \\
 & \pired &   \component{r_0}{\overline{z_0}} \parallel \overline{p_{s}} \parallel S \\
 & \equiv & \encp{(s, 0, m_1)}{\mmn{1}}
 \end{eqnarray*}
as desired.
\end{description}

\noindent\underline{\emph{Item (2)}:} 
We have a Minsky configuration $(i, m_{0}, m_1)$ with
$(i: \mathtt{HALT})$. By Definition \ref{def:confe1}, 
its encoding into \evol{1} is as follows:
\begin{eqnarray*}
\encp{(i, m_{0}, m_1)}{\mmn{1}} \! \! \!  & = &    
p_{i} \parallel \encp{r_0 = m_{0}}{\mmn{1}} \parallel \encp{r_1 = m_1}{\mmn{1}} \\&& \parallel  
  \encp{(i: \mathtt{HALT})}{\mmn{1}} \parallel   \prod_{l=1..n,\, l\not = i} \encp{(l:I_l)}{\mmn{1}} \\
   & \equiv &  \overline{p_i} \parallel !p_i.(e + \outC{p_i}) \parallel  S = P_{0}
\end{eqnarray*}
where $S = \encp{r_0 = m_{0}}{\mmn{1}} \parallel \encp{r_1 = m_1}{\mmn{1}} \parallel  \prod_{l=1..n,\, l\not = i} \encp{(l:I_l)}{\mmn{1}}$
stands for the part of the system that is not able to interact. 
It is easy to see that $P_{0} \Downarrow_{e}^1$. 
In fact, by synchronizing on $p_{i}$ and 
choosing the left-hand side process in the binary sum, we have  
$P_{0} \pired \arro{~e~}$.
The thesis is easily seen to hold by 
observing that by releasing new copies of the encoding of $(i: \mathtt{HALT})$, one always reaches a derivative $P_{j}$ of $P_{0}$
such that $P_{j} \Downarrow_{e}$.
\end{proof}



\begin{lemma}[Soundness]\label{l:sound-pas} 
Let $(i,m_0,m_1)$ be a configuration of a \mm $N$.  \\ %Then  one of the following holds: \\  %Consider a process $P = $.
If $\encp{(i,m_0,m_1)}{\mmn{1}}  \pired P_1$ then either:
\begin{enumerate}
\item 
For every computation of $P_1$ there  exists a $P_j$ such that 
$$P_{1} \pired^{*} P_j = \encp{(i',m'_0,m'_1)}{\mmn{1}}$$ and $(i,m_0,m_1)\minskred (i',m'_0,m'_1)$; or  
\item 
$P_{1} \barbk{e}$ and  $(i,m_0,m_1) \notminskred$.
\end{enumerate}
\end{lemma}
 
\begin{proof}
Consider the reduction  $\encp{(i,m_0,m_1)}{\mmn{1}}  \pired P_1$. An analysis of the structure of process
 $\encp{(i,m_0,m_1)}{\mmn{1}}$ reveals that, in all cases, the only possibility for the first step corresponds to the
consumption of the program counter $p_i$. This implies that there exists an instruction
labeled with $i$, that can be executed from the configuration $(i,m_0,m_1)$.
%That is, there exists a configuration  $(i',m'_0,m'_1)$ such that  $(i,m_0,m_1) \minskred (i',m'_0,m'_1)$.
We proceed by a case analysis on the possible instruction, considering also the 
fact that the register on which the instruction acts can hold a value equal or greater than zero.

In the cases in which $(i:\mathtt{INC}(r_{j}))$ or $(i:\mathtt{DEC}(r_{j},s))$, it can be shown that computation evolves %(nearly) 
deterministically
until reaching a process in which a new program counter (that is, some $\overline{p_{i'}}$) appears.
The program counter $\overline{p_{i'}}$ is always inside a process that corresponds to $\encp{(i',m'_0,m'_1)}{\mmn{1}}$,
where $(i,m_0,m_1)\minskred (i',m'_0,m'_1)$.  
That is, for the cases $(i:\mathtt{INC}(r_{j}))$ and $(i:\mathtt{DEC}(r_{j},s))$, we have that Item (1) above holds.
The detailed analysis follows the same lines as the one reported for the proof of Lemma \ref{l:compl-pas}, and we omit it.

In the case in which $(i:\mathtt{HALT})$, 
we have that Item (2) holds. In order to see this, 
it suffices to observe that  
if $N$ does not terminate
(more precisely: if $N$ does not reach a program counter associated to a $\mathtt{HALT}$ instruction) 
then $\encp{N}{\mmn{1}}$ does not have a barb on $e$. In fact, 
by a simple inspection on the encodings in Table~\ref{t:encod-pas}
we can deduce that $e$ 
only appears in the encoding of halt instructions, and 
does not occur in the encodings of increment and decrement-and-jump instructions.
Hence, a barb on $e$ can only be observed when $P_{1}$ is the result of triggering a halt instruction.
\end{proof}

We are now ready to repeat the statement of Lemma \ref{th:corrE1}, in Page \pageref{th:corrE1}:

\begin{lemma}[\ref{th:corrE1}]
Let $N$ be a \mm and $k \geq 1$. $N$ terminates iff $\encp{N}{1} \barbk{e}$.
\end{lemma}

\begin{proof}
It follows directly from Lemmas \ref{l:compl-pas} and \ref{l:sound-pas}.
\end{proof}
